XT: Formalizing Programming Languages in Lean
In this project, you will implement the semantics (e.g. interpreter or operational semantics) and type systems of very simple languages and prove properties about them.
For this, you will use Lean, which is both a programming language and a theorem prover.
The book Formal Reasoning about Programs would serve as an inspiration for potential formalizations. In particular, you could explore the "mixed embeddings" (see References) technique, which claims to simplify the formalization of languages considerably.